<html>
<head>
<title>pGCL formalized in HOL</title>
</head>

<body>
<h1>pGCL formalized in HOL</h1>

<h2>Overview</h2>

<p>This is a HOL formalization of pGCL (the Probabilistic Guarded
Command Language), featuring
<ul><li>a proof that weakest precondition
expectation transformers are healthy,</li>
<li>a verification condition generator for pGCL programs,
and</li><li>a verification of the probabilistic voting scheme of
Rabin's mutual exclusion protocol.</li></ul></p>

<p>To build the formalization, type <kbd>make</kbd> in the
<kbd>examples/pgcl</kbd> directory. You can clean everything by
typing <kbd>make clean</kbd> in the same directory.</p>

<h2>History</h2>

<p>The formalization was initially created by Joe Hurd while visiting
Annabelle McIver and Carroll Morgan in December 2002.</p>

<p>Aaron Coble ported the formalization to the latest version of HOL4
in May 2006.</p>

<h2>Files</h2>

The following provides a brief annotation of the theory
(<kbd>*Script</kbd>), tool (<kbd>*Tools</kbd>), library
(<kbd>*Lib</kbd>) and example files developed so far.

<h3><a href="../src/posetScript.sml"><kbd>posetScript.sml</kbd></a></h3>

Sets up the foundational theory of partially-ordered sets (posets),
leading up to the theory of complete lattices and the Knaster-Tarski
theorem. This is needed to define fixed-points over expectations.

<h3><a href="../src/posrealScript.sml"><kbd>posrealScript.sml</kbd></a></h3>

The theory of positive reals (posreals), where a positive real lies
between 0 and +infinity inclusive. This is mainly just a lifting of
useful results from realTheory.

<h3><a href="../src/posrealTools.sig"><kbd>posrealTools.sig</kbd></a><br />
<a href="../src/posrealTools.sml"><kbd>posrealTools.sml</kbd></a></h3>

Proof tools for reasoning about posreals, including:
<ul>
<li>simplification sets for
<ul>
<li>general use (<kbd>posreal_ss</kbd>),</li>
<li>performing rational number calculations (<kbd>posreal_reduce_ss</kbd>);</li>
</ul>
<li>case-splitting tactics that split posreals into
<ul>
<li>finite and infinite (<kbd>pcases</kbd>),</li>
<li>and zero, finite non-zero and infinite (<kbd>pcases3</kbd>);</li>
</ul>
<li>an associative-commutative (AC) rewriter for normalizing
multiplications (<kbd>permute_mul_conv</kbd>).
</ul>

<h3><a href="../src/posrealLib.sig"><kbd>posrealLib.sig</kbd></a><br />
<a href="../src/posrealLib.sml"><kbd>posrealLib.sml</kbd></a></h3>

At the moment this library only contains the tools in
<kbd>posrealTools</kbd>, but more may be added in the future.

<h3><a href="../src/expectationScript.sml"><kbd>expectationScript.sml</kbd></a></h3>

The theory of expectation transformers, including: the definition and
consequences of the healthiness condition; least and greatest
fixed-points; and a basic theory of refinement.

<h3><a href="../src/wpScript.sml"><kbd>wpScript.sml</kbd></a></h3>

This theory defines a miniature programming language with
probabilistic choice, demonic choice and while loops, and defines
weakest precondition (<kbd>wp</kbd>) and weakest liberal precondition
(<kbd>wlp</kbd>) semantic operators from programs to expectation
transformers. The main result is that all programs give rise to
healthy expectation transformers.

<h3><a href="../src/wpTools.sig"><kbd>wpTools.sig</kbd></a><br />
<a href="../src/wpTools.sml"><kbd>wpTools.sml</kbd></a></h3>

Tools for reasoning about <kbd>wp</kbd> and <kbd>wlp</kbd>. The most
useful tool at present is a verification condition generator tactic
<kbd>wlp_tac</kbd> for reducing goals of the form <kbd>Leq pre (wlp
prog post)</kbd>.

<h3><a href="../src/pgclLib.sig"><kbd>pgclLib.sig</kbd></a><br />
<a href="../src/pgclLib.sml"><kbd>pgclLib.sml</kbd></a></h3>

At the moment this library only contains the tools in
<kbd>wpTools</kbd>, but more may be added in the future.

<h3><a href="../src/qtl"><kbd>qtlScript.sml</kbd></a></h3>

A theory of quantative temporal logic (qtl) where the semantics are
defined in terms of expectation transformers. <font color="red">This
theory is currently broken.</font>

<h3><a href="../examples/verification.sml"><kbd>verification.sml</kbd></a></h3>

A collection of example verifications of pGCL programs:

<ul>

<li>An example illustrating how probability can be used to defeat a
demon.</li>

<li>Infinite loops: <kbd>wp</kbd> and <kbd>wlp</kbd> semantics.</li>

<li>The Monty Hall game: verification of total correctness.</li>

<li>The simple symmetric random walk: just the definition.</li>

<li>Rabin's mutual exclusion algorithm: partial correctness
verification of the probabilistic voting scheme.</li>

</ul>

</body>

</html>
